Nuprl Definition : ma-init-val 0,22

M.init(x)?v == 1of(2of(2of(M)))(x)?v 
latex



clarification:

M.init(x)?v == fpf-cap(1of(2of(2of(M)));IdDeq;x;v
latex


DefinitionsIdDeq, 2of(t), 1of(t), f(x)?z
FDL editor aliasesma-init-val

origin